Inference at * 1 
Iof proof for Lemma branch wf2:

.....subterm..... T:t1:n

1. P : 
2. d : Dec(P)
3. T : Type
4. PT
5. q:P.T
  d  (P + (P)) 

latex

 by ((RepUR ``decidable or`` 2) 
CollapseTHEN (Auto)) 

latex

Co.

Definitions

Dec(P), P  Q, t  T